\documentclass{article} % 声明文档类型为「文章」（适合短篇报告，可选 book/report 等）
\usepackage[UTF8]{ctex} % 加载 ctex 宏包（支持中文），utf8编码
\usepackage{graphicx}
\usepackage{amsmath} % 添加数学包支持
\usepackage{amssymb}
\usepackage{zed-csp}

% 自定义 section 编号格式为中文数字
\renewcommand{\thesection}{\chinese{section}}
% 二级标题用"阿拉伯数字.阿拉伯数字"
\renewcommand{\thesubsection}{\arabic{section}.\arabic{subsection}}

% 文档正文开始（此后内容会被编译显示）
\begin{document}

\begin{center} % 开启「居中」环境（使内部内容水平居中）
% \tiny（极小）→ \scriptsize → \footnotesize → \small → \normalsize（默认）→ \large → \Large → \LARGE → \huge → \Huge（依次增大）。
% bold font : bf 加粗字体
{\LARGE\textbf{实验四 \ Z的类型系统与构造单元的基本语法与规则}} \\
\vspace{0.5em} % 增加标题与信息间的垂直间距
\normalsize\textbf{
姓名: \underline{\ \normalfont 李豆豆 \ } \ 
学号: \underline{\ \normalfont 202213216 \ } \ 
专业: \underline{\ \normalfont 软件工程 \ } \
评分: \underline{\ \normalfont \quad \quad \quad }
}
\end{center}

\section{实验目的}
会用LaTex编辑集合、对象部分的形式化语言，熟悉Z语言的使用，并生成pdf文件。

\section{实验设备}
可上网计算机。

\section{软件工具的实验内容及步骤}
    \subsection{实验内容：}
        

        \begin{schema}{BOOK}
            title : TITLE\\
            author : AUTHOR\\
            subject : SUBJECT\\
            copy : COPY
        \end{schema}

        \begin{schema}{USER}
        userType : \{staff, borrowers\}\\
        actions : \mathbf{IF}\ userType = staff\ \mathbf{THEN}\ \{counterTransaction, stackTransaction, queryTransaction\}\\
        \quad\mathbf{ELSE}\ \{\}\ \mathbf{FI}
        \end{schema}

        \begin{schema}{DB}
        books : \mathbb{P} BOOK\\
        users : \mathbb{P} USER\\
        operations : \{create, read, update, delete\}
        \end{schema}


\end{document}
           

    \subsection{实验步骤：}
         \begin{enumerate}
            \item "c是欧洲的任何一个城市，则SaoPaulo面积大于c"的形式化表达：
            \[\forall c : City | c \in Europe \bullet area(SaoPaulo) > area(c)\]

            \item 定义$R=\{a,b\}$, $S=\{1,2,3\}$, 求下列笛卡尔积：
            \[R \times R = \{(a,a), (a,b), (b,a), (b,b)\}\]
            \[R \times S = \{(a,1), (a,2), (a,3), (b,1), (b,2), (b,3)\}\]
            \[R \times \mathbb{N} = \{(a,n), (b,n) | n \in \mathbb{N}\}\]

            \item 假定在图书馆系统中，一本书的每一个复本可由书和复本号来识别。如果要写该系统的规格说明，可将每一个复本表示为$Book \times \mathbb{Z}$的序偶。若以一个特定的变量newestbook来表示最近刚进入到书库的书，则可以写成声明：
            \[newestbook : Book \times \mathbb{Z}\]

            一个图书馆library可看成书的复本的集合，写出library的声明：
            \[library : \mathbb{P}(Book \times \mathbb{Z})\]

            \item "对$\mathbb{Z}$的某一个子集S和一个整数x，x是S的一个元素，x等于S中元素的个数"的形式化表达：
            \[\exists S : \mathbb{P}\mathbb{Z}; x : \mathbb{Z} \bullet x \in S \land x = \#S\]

            \item "对所有的满足x>y的x和y，x-y属于$\mathbb{N}_1$"的形式化表达：
            \[\forall x,y : \mathbb{Z} | x > y \bullet x-y \in \mathbb{N}_1\]

            \item "对于所有的Decs，如果Constr被满足，则Pred一定被满足"的两种形式化表达：
            \[\forall Decs | Constr \bullet Pred\]
            \[\forall Decs \bullet Constr \implies Pred\]

            \item 对"SaoPaulo is bigger than any other city in the same country"的谓词形式描述：
            \[\forall c : City | c \in country(SaoPaulo) \land c \neq SaoPaulo \bullet area(SaoPaulo) > area(c)\]
        \end{enumerate}

    \subsection{实验心得：}
        \indent 通过本次实验，我深入学习了Z语言中类型系统与构造单元的基本语法和规则。在实验过程中，我掌握了如何使用LaTeX编写各种形式化表达式，包括全称量词、存在量词、笛卡尔积等数学符号的使用。特别是在处理集合论和谓词逻辑的应用时，理解了如何准确地表达系统规约。这些知识和技能对于今后进行形式化建模和系统规约都很有帮助。同时，通过编写这些形式化表达式，也加深了我对Z语言本身的理解。

\end{document}
